import Lake
open Lake DSL

package "LeanProject" where
  version := v!"0.1.0"
  keywords := #["math"]
  leanOptions := #[
    ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
    ⟨`autoImplicit, false⟩
  ]

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git" @ s!"v{Lean.versionString}"
  
@[default_target]
lean_lib «LeanProject» where
  -- add any library configuration options here

lean_lib «Hello» where
lean_lib «MyTactic» where

@[default_target]
lean_exe "hello" where
  root := `Hello.Greet

@[default_target]
lean_exe "demo" where
  root := `Hello.Demo

-- 使用 lake run greet 或者 lake run greet -- "Rex..."
script "greet" (args) do
  if h : 0 < args.length then
    IO.println s!"Hello, {args[0]'h}!"
  else
    IO.println "Hello, world!"
  return 0
  
@[test_driver]
lean_exe test {
  root := `Tests.Main
}